\begin{tabbing}
$\forall$$i$, $a$:Id, $q$:FinProbSpace, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow\mathbb{B}$).
\\[0ex]@$i$ \=(with ds: ${\it ds}$\+
\\[0ex]action $a$:$q$
\\[0ex]precondition $a$ is
\\[0ex]$P$ s) 
\-\\[0ex]realizes ${\it es}$.
\\[0ex]@$i$ \=Precondition for $a$:Outcome($q$) is \+
\\[0ex]$P$:State(${\it ds}$)$\rightarrow$ $\mathbb{B}$
\-
\end{tabbing}